[[$X$]]($e$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if in{-}interface(${\it es}$;$X$;$e$) then interface{-}val(${\it es}$;$X$;$e$) else inr $\cdot$  fi